Trong toán học, một luận cứ có thể được hình thức hóa bằng lôgic biểu tượng. Khi đó, một luận cứ được coi là một danh sách có thứ tự của các mệnh đề, mỗi mệnh đề trong đó là một trong các tiền đề hoặc được rút ra từ tổ hợp của một tập con nào đó của các mệnh đề đứng trước và một hoặc nhiều tiên đề bằng cách sử dụng các luật suy luận. Mệnh đề cuối cùng trong danh sách là kết luận. Đa số các luận cứ được dùng trong các chứng minh toán học là chặt chẽ, nhưng không hình thức. Trong thực tế, việc xây dựng các chứng minh thật sự hình thức cho tất cả trừ những khẳng định tầm thường nhất đều là cực kỳ khó; các chứng minh này cũng rất khó hiểu nếu không có sự trợ giúp của máy tính. Một trong các mục đích của lĩnh vực nghiên cứu chứng minh định lý tự động là để thiết kế các chương trình máy tính để tạo và kiểm tra các chứng minh hình thức.

Một ngành nghiên cứu về các hệ thống toán học hình thức cùng với các câu hỏi ngữ nghĩa chẳng hạn như tính đầy đủ (completeness) và tính hiệu lực thường được gọi là siêu toán học (metamathematics). Một điểm lưu ý đặc biệt theo hướng này là định lý Gödel về tính không đầy đủ dành cho các lý thuyết bậc nhất về số học (first order theories of arithmetic).